We consider extensions of the two-variable guarded fragment, GF2, wheredistinguished binary predicates that occur only in guards are required to beinterpreted in a special way (as transitive relations, equivalence relations,pre-orders or partial orders). We prove that the only fragment that retains thefinite (exponential) model property is GF2 with equivalence guards withoutequality. For remaining fragments we show that the size of a minimal finitemodel is at most doubly exponential. To obtain the result we invent a strategyof building finite models that are formed from a number of multidimensionalgrids placed over a cylindrical surface. The construction yields a2NExpTime-upper bound on the complexity of the finite satisfiability problemfor these fragments. We improve the bounds and obtain optimal ones for all thefragments considered, in particular NExpTime for GF2 with equivalence guards,and 2ExpTime for GF2 with transitive guards. To obtain our results weessentially use some results from integer programming.
展开▼
